| Definitions | hd(l), i< j, i j, l[i],  A, P  Q, i j, ||as||, a<b, Case b of inl(x)  s(x) ; inr(y) t(y), kind(e), left+right, s = t, A & B,  x:A. B(x), E, A/x,y. B(x;y), 1of(t), type List, x:A B(x), ES, Void,  x:A. B(x), Top, AtomFree(T;x), tag(k), lnk(k), isrcv(k), let x = a in b(x), when-after(e;info;pred?;init;Trans;val), state_when(e), outr(x), act(k), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), Msg(M), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), source(l), SWellFounded(R(x;y)), destination(l), loc(e), "$token", outl(x), pred(e), isl(x), first(e), pred!(e;e'), if a=b c ; d fi, i=j, rel_exp(T;R;n), x f y,   , R^+, e < e', link(e), *,  , sender(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv?(e), EOrderAxioms(E; pred?; info), t  T, Unit,  , x:A  B(x), EqDecider(T), Atom$n, Id, IdLnk, es_info(es), <a,b>, inl(x), rcv(l,tg), 2of(t), inr(x), locl(a), tl(l), n-m, if a<b c ; d fi, b, if b t else f fi, nth_tl(n;as), n+m, Case of a; nil s ; x.y, rec:z t(x;y;z),  x.A(x), Y, AB,  , {x:A| B(x) }, , car.cdr,  x:A. B(x), P  Q, x(s1,s2), P  Q, P & Q, P Q, False, x when e, (x after e), f(a), Type, Prop, Dec(P), e@i. P(e), {T}, SQType(T), s ~ t, vartype(i;x), loc(e), @i stable state.P(state) , es-frame(es;i;L;x;T), x. t(x), Knd, as @ bs, kind(e), (x l) |